0 Prolog
↳1 PrologToPrologProblemTransformerProof (⇒, 86 ms)
↳2 Prolog
↳3 PrologToPiTRSProof (⇒, 29 ms)
↳4 PiTRS
↳5 DependencyPairsProof (⇔, 79 ms)
↳6 PiDP
↳7 DependencyGraphProof (⇔, 0 ms)
↳8 PiDP
↳9 UsableRulesProof (⇔, 0 ms)
↳10 PiDP
↳11 PiDPToQDPProof (⇒, 52 ms)
↳12 QDP
↳13 MRRProof (⇔, 38 ms)
↳14 QDP
↳15 PisEmptyProof (⇔, 0 ms)
↳16 YES
averageA_in_gga(0, 0, 0) → averageA_out_gga(0, 0, 0)
averageA_in_gga(0, s(0), 0) → averageA_out_gga(0, s(0), 0)
averageA_in_gga(0, s(s(0)), s(0)) → averageA_out_gga(0, s(s(0)), s(0))
averageA_in_gga(s(0), 0, 0) → averageA_out_gga(s(0), 0, 0)
averageA_in_gga(s(0), s(0), s(0)) → averageA_out_gga(s(0), s(0), s(0))
averageA_in_gga(s(s(T23)), T24, T26) → U1_gga(T23, T24, T26, averageA_in_gga(T23, s(s(T24)), T26))
averageA_in_gga(s(T39), s(s(T40)), s(T42)) → U2_gga(T39, T40, T42, averageA_in_gga(s(T39), T40, T42))
averageA_in_gga(s(T49), s(s(s(T50))), s(T52)) → U3_gga(T49, T50, T52, averageA_in_gga(s(s(T49)), T50, T52))
averageA_in_gga(T74, s(s(s(T75))), s(T77)) → U4_gga(T74, T75, T77, averageA_in_gga(T74, s(T75), T77))
averageA_in_gga(T84, s(s(s(s(s(s(T85)))))), s(s(T87))) → U5_gga(T84, T85, T87, averageA_in_gga(s(s(T84)), T85, T87))
U5_gga(T84, T85, T87, averageA_out_gga(s(s(T84)), T85, T87)) → averageA_out_gga(T84, s(s(s(s(s(s(T85)))))), s(s(T87)))
U4_gga(T74, T75, T77, averageA_out_gga(T74, s(T75), T77)) → averageA_out_gga(T74, s(s(s(T75))), s(T77))
U3_gga(T49, T50, T52, averageA_out_gga(s(s(T49)), T50, T52)) → averageA_out_gga(s(T49), s(s(s(T50))), s(T52))
U2_gga(T39, T40, T42, averageA_out_gga(s(T39), T40, T42)) → averageA_out_gga(s(T39), s(s(T40)), s(T42))
U1_gga(T23, T24, T26, averageA_out_gga(T23, s(s(T24)), T26)) → averageA_out_gga(s(s(T23)), T24, T26)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
averageA_in_gga(0, 0, 0) → averageA_out_gga(0, 0, 0)
averageA_in_gga(0, s(0), 0) → averageA_out_gga(0, s(0), 0)
averageA_in_gga(0, s(s(0)), s(0)) → averageA_out_gga(0, s(s(0)), s(0))
averageA_in_gga(s(0), 0, 0) → averageA_out_gga(s(0), 0, 0)
averageA_in_gga(s(0), s(0), s(0)) → averageA_out_gga(s(0), s(0), s(0))
averageA_in_gga(s(s(T23)), T24, T26) → U1_gga(T23, T24, T26, averageA_in_gga(T23, s(s(T24)), T26))
averageA_in_gga(s(T39), s(s(T40)), s(T42)) → U2_gga(T39, T40, T42, averageA_in_gga(s(T39), T40, T42))
averageA_in_gga(s(T49), s(s(s(T50))), s(T52)) → U3_gga(T49, T50, T52, averageA_in_gga(s(s(T49)), T50, T52))
averageA_in_gga(T74, s(s(s(T75))), s(T77)) → U4_gga(T74, T75, T77, averageA_in_gga(T74, s(T75), T77))
averageA_in_gga(T84, s(s(s(s(s(s(T85)))))), s(s(T87))) → U5_gga(T84, T85, T87, averageA_in_gga(s(s(T84)), T85, T87))
U5_gga(T84, T85, T87, averageA_out_gga(s(s(T84)), T85, T87)) → averageA_out_gga(T84, s(s(s(s(s(s(T85)))))), s(s(T87)))
U4_gga(T74, T75, T77, averageA_out_gga(T74, s(T75), T77)) → averageA_out_gga(T74, s(s(s(T75))), s(T77))
U3_gga(T49, T50, T52, averageA_out_gga(s(s(T49)), T50, T52)) → averageA_out_gga(s(T49), s(s(s(T50))), s(T52))
U2_gga(T39, T40, T42, averageA_out_gga(s(T39), T40, T42)) → averageA_out_gga(s(T39), s(s(T40)), s(T42))
U1_gga(T23, T24, T26, averageA_out_gga(T23, s(s(T24)), T26)) → averageA_out_gga(s(s(T23)), T24, T26)
AVERAGEA_IN_GGA(s(s(T23)), T24, T26) → U1_GGA(T23, T24, T26, averageA_in_gga(T23, s(s(T24)), T26))
AVERAGEA_IN_GGA(s(s(T23)), T24, T26) → AVERAGEA_IN_GGA(T23, s(s(T24)), T26)
AVERAGEA_IN_GGA(s(T39), s(s(T40)), s(T42)) → U2_GGA(T39, T40, T42, averageA_in_gga(s(T39), T40, T42))
AVERAGEA_IN_GGA(s(T39), s(s(T40)), s(T42)) → AVERAGEA_IN_GGA(s(T39), T40, T42)
AVERAGEA_IN_GGA(s(T49), s(s(s(T50))), s(T52)) → U3_GGA(T49, T50, T52, averageA_in_gga(s(s(T49)), T50, T52))
AVERAGEA_IN_GGA(s(T49), s(s(s(T50))), s(T52)) → AVERAGEA_IN_GGA(s(s(T49)), T50, T52)
AVERAGEA_IN_GGA(T74, s(s(s(T75))), s(T77)) → U4_GGA(T74, T75, T77, averageA_in_gga(T74, s(T75), T77))
AVERAGEA_IN_GGA(T74, s(s(s(T75))), s(T77)) → AVERAGEA_IN_GGA(T74, s(T75), T77)
AVERAGEA_IN_GGA(T84, s(s(s(s(s(s(T85)))))), s(s(T87))) → U5_GGA(T84, T85, T87, averageA_in_gga(s(s(T84)), T85, T87))
AVERAGEA_IN_GGA(T84, s(s(s(s(s(s(T85)))))), s(s(T87))) → AVERAGEA_IN_GGA(s(s(T84)), T85, T87)
averageA_in_gga(0, 0, 0) → averageA_out_gga(0, 0, 0)
averageA_in_gga(0, s(0), 0) → averageA_out_gga(0, s(0), 0)
averageA_in_gga(0, s(s(0)), s(0)) → averageA_out_gga(0, s(s(0)), s(0))
averageA_in_gga(s(0), 0, 0) → averageA_out_gga(s(0), 0, 0)
averageA_in_gga(s(0), s(0), s(0)) → averageA_out_gga(s(0), s(0), s(0))
averageA_in_gga(s(s(T23)), T24, T26) → U1_gga(T23, T24, T26, averageA_in_gga(T23, s(s(T24)), T26))
averageA_in_gga(s(T39), s(s(T40)), s(T42)) → U2_gga(T39, T40, T42, averageA_in_gga(s(T39), T40, T42))
averageA_in_gga(s(T49), s(s(s(T50))), s(T52)) → U3_gga(T49, T50, T52, averageA_in_gga(s(s(T49)), T50, T52))
averageA_in_gga(T74, s(s(s(T75))), s(T77)) → U4_gga(T74, T75, T77, averageA_in_gga(T74, s(T75), T77))
averageA_in_gga(T84, s(s(s(s(s(s(T85)))))), s(s(T87))) → U5_gga(T84, T85, T87, averageA_in_gga(s(s(T84)), T85, T87))
U5_gga(T84, T85, T87, averageA_out_gga(s(s(T84)), T85, T87)) → averageA_out_gga(T84, s(s(s(s(s(s(T85)))))), s(s(T87)))
U4_gga(T74, T75, T77, averageA_out_gga(T74, s(T75), T77)) → averageA_out_gga(T74, s(s(s(T75))), s(T77))
U3_gga(T49, T50, T52, averageA_out_gga(s(s(T49)), T50, T52)) → averageA_out_gga(s(T49), s(s(s(T50))), s(T52))
U2_gga(T39, T40, T42, averageA_out_gga(s(T39), T40, T42)) → averageA_out_gga(s(T39), s(s(T40)), s(T42))
U1_gga(T23, T24, T26, averageA_out_gga(T23, s(s(T24)), T26)) → averageA_out_gga(s(s(T23)), T24, T26)
AVERAGEA_IN_GGA(s(s(T23)), T24, T26) → U1_GGA(T23, T24, T26, averageA_in_gga(T23, s(s(T24)), T26))
AVERAGEA_IN_GGA(s(s(T23)), T24, T26) → AVERAGEA_IN_GGA(T23, s(s(T24)), T26)
AVERAGEA_IN_GGA(s(T39), s(s(T40)), s(T42)) → U2_GGA(T39, T40, T42, averageA_in_gga(s(T39), T40, T42))
AVERAGEA_IN_GGA(s(T39), s(s(T40)), s(T42)) → AVERAGEA_IN_GGA(s(T39), T40, T42)
AVERAGEA_IN_GGA(s(T49), s(s(s(T50))), s(T52)) → U3_GGA(T49, T50, T52, averageA_in_gga(s(s(T49)), T50, T52))
AVERAGEA_IN_GGA(s(T49), s(s(s(T50))), s(T52)) → AVERAGEA_IN_GGA(s(s(T49)), T50, T52)
AVERAGEA_IN_GGA(T74, s(s(s(T75))), s(T77)) → U4_GGA(T74, T75, T77, averageA_in_gga(T74, s(T75), T77))
AVERAGEA_IN_GGA(T74, s(s(s(T75))), s(T77)) → AVERAGEA_IN_GGA(T74, s(T75), T77)
AVERAGEA_IN_GGA(T84, s(s(s(s(s(s(T85)))))), s(s(T87))) → U5_GGA(T84, T85, T87, averageA_in_gga(s(s(T84)), T85, T87))
AVERAGEA_IN_GGA(T84, s(s(s(s(s(s(T85)))))), s(s(T87))) → AVERAGEA_IN_GGA(s(s(T84)), T85, T87)
averageA_in_gga(0, 0, 0) → averageA_out_gga(0, 0, 0)
averageA_in_gga(0, s(0), 0) → averageA_out_gga(0, s(0), 0)
averageA_in_gga(0, s(s(0)), s(0)) → averageA_out_gga(0, s(s(0)), s(0))
averageA_in_gga(s(0), 0, 0) → averageA_out_gga(s(0), 0, 0)
averageA_in_gga(s(0), s(0), s(0)) → averageA_out_gga(s(0), s(0), s(0))
averageA_in_gga(s(s(T23)), T24, T26) → U1_gga(T23, T24, T26, averageA_in_gga(T23, s(s(T24)), T26))
averageA_in_gga(s(T39), s(s(T40)), s(T42)) → U2_gga(T39, T40, T42, averageA_in_gga(s(T39), T40, T42))
averageA_in_gga(s(T49), s(s(s(T50))), s(T52)) → U3_gga(T49, T50, T52, averageA_in_gga(s(s(T49)), T50, T52))
averageA_in_gga(T74, s(s(s(T75))), s(T77)) → U4_gga(T74, T75, T77, averageA_in_gga(T74, s(T75), T77))
averageA_in_gga(T84, s(s(s(s(s(s(T85)))))), s(s(T87))) → U5_gga(T84, T85, T87, averageA_in_gga(s(s(T84)), T85, T87))
U5_gga(T84, T85, T87, averageA_out_gga(s(s(T84)), T85, T87)) → averageA_out_gga(T84, s(s(s(s(s(s(T85)))))), s(s(T87)))
U4_gga(T74, T75, T77, averageA_out_gga(T74, s(T75), T77)) → averageA_out_gga(T74, s(s(s(T75))), s(T77))
U3_gga(T49, T50, T52, averageA_out_gga(s(s(T49)), T50, T52)) → averageA_out_gga(s(T49), s(s(s(T50))), s(T52))
U2_gga(T39, T40, T42, averageA_out_gga(s(T39), T40, T42)) → averageA_out_gga(s(T39), s(s(T40)), s(T42))
U1_gga(T23, T24, T26, averageA_out_gga(T23, s(s(T24)), T26)) → averageA_out_gga(s(s(T23)), T24, T26)
AVERAGEA_IN_GGA(s(T39), s(s(T40)), s(T42)) → AVERAGEA_IN_GGA(s(T39), T40, T42)
AVERAGEA_IN_GGA(s(s(T23)), T24, T26) → AVERAGEA_IN_GGA(T23, s(s(T24)), T26)
AVERAGEA_IN_GGA(s(T49), s(s(s(T50))), s(T52)) → AVERAGEA_IN_GGA(s(s(T49)), T50, T52)
AVERAGEA_IN_GGA(T74, s(s(s(T75))), s(T77)) → AVERAGEA_IN_GGA(T74, s(T75), T77)
AVERAGEA_IN_GGA(T84, s(s(s(s(s(s(T85)))))), s(s(T87))) → AVERAGEA_IN_GGA(s(s(T84)), T85, T87)
averageA_in_gga(0, 0, 0) → averageA_out_gga(0, 0, 0)
averageA_in_gga(0, s(0), 0) → averageA_out_gga(0, s(0), 0)
averageA_in_gga(0, s(s(0)), s(0)) → averageA_out_gga(0, s(s(0)), s(0))
averageA_in_gga(s(0), 0, 0) → averageA_out_gga(s(0), 0, 0)
averageA_in_gga(s(0), s(0), s(0)) → averageA_out_gga(s(0), s(0), s(0))
averageA_in_gga(s(s(T23)), T24, T26) → U1_gga(T23, T24, T26, averageA_in_gga(T23, s(s(T24)), T26))
averageA_in_gga(s(T39), s(s(T40)), s(T42)) → U2_gga(T39, T40, T42, averageA_in_gga(s(T39), T40, T42))
averageA_in_gga(s(T49), s(s(s(T50))), s(T52)) → U3_gga(T49, T50, T52, averageA_in_gga(s(s(T49)), T50, T52))
averageA_in_gga(T74, s(s(s(T75))), s(T77)) → U4_gga(T74, T75, T77, averageA_in_gga(T74, s(T75), T77))
averageA_in_gga(T84, s(s(s(s(s(s(T85)))))), s(s(T87))) → U5_gga(T84, T85, T87, averageA_in_gga(s(s(T84)), T85, T87))
U5_gga(T84, T85, T87, averageA_out_gga(s(s(T84)), T85, T87)) → averageA_out_gga(T84, s(s(s(s(s(s(T85)))))), s(s(T87)))
U4_gga(T74, T75, T77, averageA_out_gga(T74, s(T75), T77)) → averageA_out_gga(T74, s(s(s(T75))), s(T77))
U3_gga(T49, T50, T52, averageA_out_gga(s(s(T49)), T50, T52)) → averageA_out_gga(s(T49), s(s(s(T50))), s(T52))
U2_gga(T39, T40, T42, averageA_out_gga(s(T39), T40, T42)) → averageA_out_gga(s(T39), s(s(T40)), s(T42))
U1_gga(T23, T24, T26, averageA_out_gga(T23, s(s(T24)), T26)) → averageA_out_gga(s(s(T23)), T24, T26)
AVERAGEA_IN_GGA(s(T39), s(s(T40)), s(T42)) → AVERAGEA_IN_GGA(s(T39), T40, T42)
AVERAGEA_IN_GGA(s(s(T23)), T24, T26) → AVERAGEA_IN_GGA(T23, s(s(T24)), T26)
AVERAGEA_IN_GGA(s(T49), s(s(s(T50))), s(T52)) → AVERAGEA_IN_GGA(s(s(T49)), T50, T52)
AVERAGEA_IN_GGA(T74, s(s(s(T75))), s(T77)) → AVERAGEA_IN_GGA(T74, s(T75), T77)
AVERAGEA_IN_GGA(T84, s(s(s(s(s(s(T85)))))), s(s(T87))) → AVERAGEA_IN_GGA(s(s(T84)), T85, T87)
AVERAGEA_IN_GGA(s(T39), s(s(T40))) → AVERAGEA_IN_GGA(s(T39), T40)
AVERAGEA_IN_GGA(s(s(T23)), T24) → AVERAGEA_IN_GGA(T23, s(s(T24)))
AVERAGEA_IN_GGA(s(T49), s(s(s(T50)))) → AVERAGEA_IN_GGA(s(s(T49)), T50)
AVERAGEA_IN_GGA(T74, s(s(s(T75)))) → AVERAGEA_IN_GGA(T74, s(T75))
AVERAGEA_IN_GGA(T84, s(s(s(s(s(s(T85))))))) → AVERAGEA_IN_GGA(s(s(T84)), T85)
AVERAGEA_IN_GGA(s(T39), s(s(T40))) → AVERAGEA_IN_GGA(s(T39), T40)
AVERAGEA_IN_GGA(s(s(T23)), T24) → AVERAGEA_IN_GGA(T23, s(s(T24)))
AVERAGEA_IN_GGA(s(T49), s(s(s(T50)))) → AVERAGEA_IN_GGA(s(s(T49)), T50)
AVERAGEA_IN_GGA(T74, s(s(s(T75)))) → AVERAGEA_IN_GGA(T74, s(T75))
AVERAGEA_IN_GGA(T84, s(s(s(s(s(s(T85))))))) → AVERAGEA_IN_GGA(s(s(T84)), T85)
s1 > AVERAGEAINGGA2
s_1=1
AVERAGEA_IN_GGA_2=0